COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input macro[1,mps]
C00015 ENDMK
C⊗;
\input macro[1,mps]
\magnification\magstephalf
\baselineskip 14pt
\leftline{\sevenrm A77.Tex[254,mps]\today}
\leftline{\copyright\sevenrm Robert W. Floyd, November 30, 1988}
\leftline{\sevenrm Unpublished draft}
\bigskip
\noindent{\bf Proofs for Takehome Final, CS 254, Spring 1985--86}

\parindent 0pt
\medskip
{\bf \# 1.} The property in question is $P(y)≡(\forall x)[x\otimes y$ is
defined].

Base step: $P(\epsilon)$ is, $x\otimes \epsilon$ is defined. Obvious.

Induction step: Assume $x\otimes y$ is defined and show $x\otimes S↓a(y)$.
The latter is $S↓a(x\otimes y)$, again obviously defined.

The above is not, however, a complete proof. It does not prevent definitions
like
$$\eqalign{f(0)&=0\cr
f(1)&=1\cr
f(x+2)&=f(x)+3\cr
f(x+3)&=f(x)+2\cr}$$
which ``define'' $f(x)$ for all natural numbers, but overdefine it so that
$f(3)=2$ and $f(3)=4$.

\smallskip
A perfectionist proof makes $P(y)≡(\forall x)(x\otimes y$ is uniquely defined),
and checks that for a given $x$ and~$y$, no multiple definition occurs.

\medskip
{\bf \# 2.} 
\disleft 25pt:{\bf (A)}:
Base: show $\epsilon\otimes\epsilon=\epsilon$. Direct by substitution
in $x\otimes \epsilon=x$. 
\disleft 25pt::
Induction step: show $\epsilon\otimes x=x$ implies
$\epsilon\otimes S↓a(x)=S↓a(x)$
$$\epsilon\otimes S↓a(x)=S↓a(\epsilon\otimes x)=S↓a(x)\,.\quad\blackslug$$

\smallskip
\disleft 25pt:{\bf (B)}:
Base: show 
$(x\otimes y)\otimes\epsilon=x\otimes (y\otimes\epsilon)$
$$(x\otimes y)\otimes\epsilon=x\otimes y=x\otimes(y\otimes\epsilon)\,.$$
Induction: show
$(x\otimes y)\otimes z =x\otimes (y\otimes z)$ implies
$(x\otimes y)\otimes S↓a(z)=x\otimes \bigl(y\otimes S↓a(z)\bigr)$.
$$\eqalign{(x\otimes y)\otimes S↓a(z)&=S↓a\bigl((x\otimes y)\otimes z\bigr)
=S↓a\bigl(x\otimes(y\otimes z)\bigr)\,,\cr
x\otimes\bigl(y\otimes S↓a(z)\bigr)&=x\otimes S↓a(y\otimes z)
=S↓a\bigl(x\otimes(y\otimes z)\bigr)\,.\quad\blackslug\cr}$$

\medskip
{\bf \# 3.} $S↓a(x)$ is, by notational convention, a function of~$x$. A relation
is a function if for each~$x$, there is exactly one pair $\langle x,y\rangle$
in the relation. In this case, $y=S↓a(x)$ is the unique possibility.

\medskip
{\bf \# 4.} $\langle y,x\rangle\in{\rm pop}\;a≡\langle x,y\rangle\in
{\rm push}\; a≡y=S↓a(x)$. It suffices to show that for each~$y$ there is
at most one such~$x$. If $y=S↓a(x↓1)$ and $y=S↓a(x↓2)$, so
$S↓a(x↓1)=S↓a(x↓2)$, then by Peano axiom~(5) $x↓1=x↓2$.

\medskip
{\bf \# 5.}
$$\eqalign{&\langle x,z\rangle\in{\rm Push}\;a\circ{\rm pop}\;a≡\cr
&(\exists y)[\langle x,y\rangle\in{\rm push}\;a∧\langle y,z\rangle\in{\rm pop}\;
a]≡\cr
&(\exists y)[\langle x,y\rangle\in{\rm push}\; a∧\langle z,y\rangle\in{\rm push}\;
a]≡\cr
&(\exists y)[y=S↓a(x)∧y=S↓a(z)]≡\cr
&S↓a(x)=S↓a(z)≡\cr
&x=z\,.\cr}$$

\medskip
{\bf \# 6.} Similarly,
$$\eqalign{&\langle x,z\rangle\in{\rm Push}\; a\circ{\rm pop}\; b≡\cr
&S↓a(x)=S↓b(y)\,,\quad\hbox{false by Peano$↓5$}.\cr}$$

\medskip
{\bf \# 7.}
\disleft 25pt:{\bf (A)}:
Show $L⊂L↓{G↓1}$.
\display 50pt:{\bf (A1)}:
$E→\epsilon$, so $\epsilon\in L↓{G↓1}$.
\display 50pt:{\bf (A2)}:
Assume $x\in L↓{G↓1}$. Then
$$\eqalign{E&→(E)E\aRa (x)E\Rightarrow (x)\epsilon =(x)\quad\hbox{and}\cr
E&→[E]E\aRa [x]E\Rightarrow [x]\epsilon =[x]\cr}$$
so $(x)$ and $[x]$ are in $L↓{G↓1}$.
\display 50pt:{\bf (A3)}:
Assume $x,y\in L↓{G↓1}$; show $xy\in L↓{G↓1}$. If $x=\epsilon$, immediate.
Otherwise $E→(E)E\aRa x$ (say); by the partition theorem $x=(x↓1)x↓2$,
$E\aRa x↓1$, $E\Rightarrow x↓2$. By course-of-values induction,
$x↓2\in L↓{G↓1}$ and $y\in L↓{G↓1}⊃x↓2y\in L↓{G↓1}$. Then
$E\aRa (E)E\aRa (x↓1)E\aRa (x↓1)x↓2y=xy$, so $xy\in L↓{G↓1}$.

\smallskip
\disleft 25pt:{\bf (B)}:
Show $L↓{G↓1}⊂L$.
\display 50pt:{\bf (B1)}:
$E→\epsilon =x$ implies $x\in L$.
\display 50pt:{\bf (B2)}:
$E→(E)E\aRa (x↓1)x↓2=x$, where by course-of-values induction
$x↓1\in L$, $x↓2\in L$, shows $(x↓1)\in L$, $x=(x↓1)x↓2\in L$.
\display 50pt:{\bf (B3)}:
Similar for $E→[E]E$.

\medskip
{\bf \# 8.}
\disleft 25pt:{\bf (A)}:
$\epsilon$ names $I↓{\Sigma↑{\ast}}$ by convention.
\disleft 25pt:{\bf (B)}:
$F→{\rm push}\; a\,F\;{\rm pop}\;a\,F\aRa{\rm push}\;a\,x↓1\;{\rm pop}\;a\,x↓2
≡{\rm push}\;a\circ I↓{\Sigma↑{\ast}}\circ{\rm pop}\;a\circ I↓{\Sigma↑{\ast}}
=I↓{\Sigma↑{\ast}}$ by Drill \# 5.
\disleft 25pt:{\bf (C)}:
Similar.

\medskip
{\bf \# 9.} A sequence of pushes and pops that contains the sequence 
push~$a$ pop~$b$ is clearly equivalent to~$\emptyset$, and so does not change
$\epsilon$ to~$\epsilon$ (as a relation, does not contain $\langle\epsilon,
\epsilon\rangle$). Nor could it begin with a pop, nor end with a push. If
not empty, looking for the first pop finds a substring push~$a$ pop~$a$.
Since push~$a\;\circ$ pop~$a≡I↓{\Sigma↑{\ast}}$, omitting it yields the same
relation, so it changes $\epsilon$ to~$\epsilon$ and is, by induction,
in~$L↓{G↓2}$. We now just need to show if $x↓1x↓2\in L↓{G↓2}$, so is
$x↓1$~push~$a$ pop~$a$~$x↓2$; to show this, we show if $F\aRa x↓1x↓2$,
then $F\aRa x↓1Fx↓2\aRa x↓1$ push~$a$ pop~$a\,x↓2$.
Equivalently, in~$L↓{G↓1}$, we show if $E\aRa x↓1x↓2$, then $E\aRa x↓1(\,)x↓2$.

\smallskip
Induction does the job.
\disleft 25pt:{\bf (1)}:
$E→\epsilon\aRa x↓1x↓2=\epsilon$; then $E\Rightarrow (E)E\Rightarrow
(\,)E\Rightarrow (\,)=x↓1(\,)x↓2$.
\disleft 25pt:{\bf (2)}:
$E→(E)E\aRa (y↓1)y↓2$. If the place we want to insert $(\,)$ is in (or next to)
$y↓1$ or~$y↓2$, course-of-values induction does it. Otherwise it is at the
start, and $E→(E)E\Rightarrow (\,)E\Rightarrow (\,)(E)E\aRa (\,)(y↓1)y↓2$.
\disleft 25pt:{\bf (3)}:
$E→[E]E$, like (2).

\smallskip
Drill \# 9 seems the hardest.

\medskip
{\bf \# 10.} A string is a computation of a PDM if it is a labeled path
through the graph and if the operations it describes on any device are
possible. The input operations on any path through a standardized PDM
are of the form 
$$\hbox{EOF? No. Read $a↓1$ EOF? No. Read $a↓2\ldots$ Read $a↓n$ EOF? Yes;}$$
clearly possible if the input is $a↓1a↓2\ldots a↓n$. The write operations
are of the form
$$\hbox{Write $b↓1$, write $b↓2$, write $b↓3,\ldots$, write $b↓n$,}$$
again possible. The stack operations are a sentence in~$G↓2$, possible
by Drill \# 8.

\medskip
{\bf \# 11.} A string $x$ is a computation of a {\sl standardized\/} PDM
(the drill is weakened here, at no harm to the further results) if
$x\circ I↓r\circ M↓{\rm omit}\circ L↓{G↓2}$, where $r$ is the regular set
of labeled paths through the graph and $M↓{\rm omit}$ is a GSM that copies
stack operations to the output and ignores other input. Since there is an
obvious GSM $M$ mapping $L↓{G↓2}$ to~$L↓{(\,)[\,]}$ for which
$L↓{G↓2}=M\circ L↓{(\,)[\,]}$, $x$~is a computation of the PDM if
$$x\circ I↓r\circ R↓{M↓{\rm omit}}\circ R↓M\circ L↓{(\,)[\,]}\,.$$
Let the desired $M'$ be the converse GSM, $M↓c$, of $I↓r\circ M↓{\rm omit}
\circ M$, so the set of computations is $L↓{(\,)[\,]}\circ R↓{M'}$.

\medskip
{\bf \# 12.} Let $L↓p$ be the set of strings accepted by a given PDM, and
therefore accepted by a standardized PDM. The set of computations of that
PDM is $L↓{(\,)[\,]}\circ M'$, by Drill \# 11; let $M''$ be a GSM that
passes only input characters of the PDM to its output; then
$L↓{(\,)[\,]}\circ (R↓{M'}\circ R↓{M''})$ is the set of strings accepted
by the PDM, and $M'\circ M''$ is the desired GSM. 

\proclaim Theorem. If a language is the image of the CFL $L↓{(\,)[\,]}$
under a GSM mapping, it is, by a theorem shown in the lectures, a CFL.
If a language is a CFL, it is accepted by a PDM, and therefore by Drill \# 12
the image of $L↓{(\,)[\,]}$ under a GSM mapping.

\bye